0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 11 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 9090 ms)
↳10 BOUNDS(1, n^2)
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs))
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) → ys
helpc(false, ys, zs) → zs
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs))
app(x, y) → helpa(0, plus(length(x), length(y)), x, y) [1]
plus(x, 0) → x [1]
plus(x, s(y)) → s(plus(x, y)) [1]
length(nil) → 0 [1]
length(cons(x, y)) → s(length(y)) [1]
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs) [1]
ge(x, 0) → true [1]
ge(0, s(x)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
if(true, c, l, ys, zs) → nil [1]
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs)) [1]
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs) [1]
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys) [1]
helpc(true, ys, zs) → ys [1]
helpc(false, ys, zs) → zs [1]
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs)) [1]
app(x, y) → helpa(0, plus(length(x), length(y)), x, y) [1]
plus(x, 0) → x [1]
plus(x, s(y)) → s(plus(x, y)) [1]
length(nil) → 0 [1]
length(cons(x, y)) → s(length(y)) [1]
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs) [1]
ge(x, 0) → true [1]
ge(0, s(x)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
if(true, c, l, ys, zs) → nil [1]
if(false, c, l, ys, zs) → helpb(c, l, greater(ys, zs), smaller(ys, zs)) [1]
greater(ys, zs) → helpc(ge(length(ys), length(zs)), ys, zs) [1]
smaller(ys, zs) → helpc(ge(length(ys), length(zs)), zs, ys) [1]
helpc(true, ys, zs) → ys [1]
helpc(false, ys, zs) → zs [1]
helpb(c, l, cons(y, ys), zs) → cons(y, helpa(s(c), l, ys, zs)) [1]
| app :: nil:cons → nil:cons → nil:cons helpa :: 0:s → 0:s → nil:cons → nil:cons → nil:cons 0 :: 0:s plus :: 0:s → 0:s → 0:s length :: nil:cons → 0:s s :: 0:s → 0:s nil :: nil:cons cons :: a → nil:cons → nil:cons if :: true:false → 0:s → 0:s → nil:cons → nil:cons → nil:cons ge :: 0:s → 0:s → true:false true :: true:false false :: true:false helpb :: 0:s → 0:s → nil:cons → nil:cons → nil:cons greater :: nil:cons → nil:cons → nil:cons smaller :: nil:cons → nil:cons → nil:cons helpc :: true:false → nil:cons → nil:cons → nil:cons |
helpb(v0, v1, v2, v3) → null_helpb [0]
length(v0) → null_length [0]
plus(v0, v1) → null_plus [0]
ge(v0, v1) → null_ge [0]
if(v0, v1, v2, v3, v4) → null_if [0]
helpc(v0, v1, v2) → null_helpc [0]
null_helpb, null_length, null_plus, null_ge, null_if, null_helpc, const
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
nil => 0
true => 2
false => 1
null_helpb => 0
null_length => 0
null_plus => 0
null_ge => 0
null_if => 0
null_helpc => 0
const => 0
app(z, z') -{ 1 }→ helpa(0, plus(length(x), length(y)), x, y) :|: x >= 0, y >= 0, z = x, z' = y
ge(z, z') -{ 1 }→ ge(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
ge(z, z') -{ 1 }→ 2 :|: x >= 0, z = x, z' = 0
ge(z, z') -{ 1 }→ 1 :|: z' = 1 + x, x >= 0, z = 0
ge(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
greater(z, z') -{ 1 }→ helpc(ge(length(ys), length(zs)), ys, zs) :|: z = ys, z' = zs, ys >= 0, zs >= 0
helpa(z, z', z'', z1) -{ 1 }→ if(ge(c, l), c, l, ys, zs) :|: z' = l, c >= 0, ys >= 0, zs >= 0, z'' = ys, z = c, l >= 0, z1 = zs
helpb(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
helpb(z, z', z'', z1) -{ 1 }→ 1 + y + helpa(1 + c, l, ys, zs) :|: z' = l, z'' = 1 + y + ys, c >= 0, ys >= 0, zs >= 0, y >= 0, z = c, l >= 0, z1 = zs
helpc(z, z', z'') -{ 1 }→ ys :|: z = 2, z' = ys, ys >= 0, zs >= 0, z'' = zs
helpc(z, z', z'') -{ 1 }→ zs :|: z' = ys, z = 1, ys >= 0, zs >= 0, z'' = zs
helpc(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if(z, z', z'', z1, z2) -{ 1 }→ helpb(c, l, greater(ys, zs), smaller(ys, zs)) :|: z2 = zs, c >= 0, z = 1, ys >= 0, zs >= 0, l >= 0, z' = c, z'' = l, z1 = ys
if(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z = 2, z2 = zs, c >= 0, ys >= 0, zs >= 0, l >= 0, z' = c, z'' = l, z1 = ys
if(z, z', z'', z1, z2) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z2 = v4, v2 >= 0, v3 >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
length(z) -{ 1 }→ 1 + length(y) :|: z = 1 + x + y, x >= 0, y >= 0
plus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
plus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
plus(z, z') -{ 1 }→ 1 + plus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = x
smaller(z, z') -{ 1 }→ helpc(ge(length(ys), length(zs)), zs, ys) :|: z = ys, z' = zs, ys >= 0, zs >= 0
| eq(start(V, V1, V9, V10, V19),0,[app(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V19),0,[plus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V19),0,[length(V, Out)],[V >= 0]). eq(start(V, V1, V9, V10, V19),0,[helpa(V, V1, V9, V10, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0]). eq(start(V, V1, V9, V10, V19),0,[ge(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V19),0,[if(V, V1, V9, V10, V19, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0,V19 >= 0]). eq(start(V, V1, V9, V10, V19),0,[greater(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V19),0,[smaller(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V19),0,[helpc(V, V1, V9, Out)],[V >= 0,V1 >= 0,V9 >= 0]). eq(start(V, V1, V9, V10, V19),0,[helpb(V, V1, V9, V10, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0]). eq(app(V, V1, Out),1,[length(V2, Ret10),length(V3, Ret11),plus(Ret10, Ret11, Ret1),helpa(0, Ret1, V2, V3, Ret)],[Out = Ret,V2 >= 0,V3 >= 0,V = V2,V1 = V3]). eq(plus(V, V1, Out),1,[],[Out = V4,V4 >= 0,V = V4,V1 = 0]). eq(plus(V, V1, Out),1,[plus(V5, V6, Ret12)],[Out = 1 + Ret12,V1 = 1 + V6,V5 >= 0,V6 >= 0,V = V5]). eq(length(V, Out),1,[],[Out = 0,V = 0]). eq(length(V, Out),1,[length(V7, Ret13)],[Out = 1 + Ret13,V = 1 + V7 + V8,V8 >= 0,V7 >= 0]). eq(helpa(V, V1, V9, V10, Out),1,[ge(V11, V12, Ret0),if(Ret0, V11, V12, V13, V14, Ret2)],[Out = Ret2,V1 = V12,V11 >= 0,V13 >= 0,V14 >= 0,V9 = V13,V = V11,V12 >= 0,V10 = V14]). eq(ge(V, V1, Out),1,[],[Out = 2,V15 >= 0,V = V15,V1 = 0]). eq(ge(V, V1, Out),1,[],[Out = 1,V1 = 1 + V16,V16 >= 0,V = 0]). eq(ge(V, V1, Out),1,[ge(V17, V18, Ret3)],[Out = Ret3,V1 = 1 + V18,V17 >= 0,V18 >= 0,V = 1 + V17]). eq(if(V, V1, V9, V10, V19, Out),1,[],[Out = 0,V = 2,V19 = V20,V21 >= 0,V22 >= 0,V20 >= 0,V23 >= 0,V1 = V21,V9 = V23,V10 = V22]). eq(if(V, V1, V9, V10, V19, Out),1,[greater(V26, V27, Ret21),smaller(V26, V27, Ret31),helpb(V24, V25, Ret21, Ret31, Ret4)],[Out = Ret4,V19 = V27,V24 >= 0,V = 1,V26 >= 0,V27 >= 0,V25 >= 0,V1 = V24,V9 = V25,V10 = V26]). eq(greater(V, V1, Out),1,[length(V28, Ret00),length(V29, Ret01),ge(Ret00, Ret01, Ret02),helpc(Ret02, V28, V29, Ret5)],[Out = Ret5,V = V28,V1 = V29,V28 >= 0,V29 >= 0]). eq(smaller(V, V1, Out),1,[length(V30, Ret001),length(V31, Ret011),ge(Ret001, Ret011, Ret03),helpc(Ret03, V31, V30, Ret6)],[Out = Ret6,V = V30,V1 = V31,V30 >= 0,V31 >= 0]). eq(helpc(V, V1, V9, Out),1,[],[Out = V32,V = 2,V1 = V32,V32 >= 0,V33 >= 0,V9 = V33]). eq(helpc(V, V1, V9, Out),1,[],[Out = V34,V1 = V35,V = 1,V35 >= 0,V34 >= 0,V9 = V34]). eq(helpb(V, V1, V9, V10, Out),1,[helpa(1 + V37, V38, V39, V40, Ret14)],[Out = 1 + Ret14 + V36,V1 = V38,V9 = 1 + V36 + V39,V37 >= 0,V39 >= 0,V40 >= 0,V36 >= 0,V = V37,V38 >= 0,V10 = V40]). eq(helpb(V, V1, V9, V10, Out),0,[],[Out = 0,V10 = V41,V42 >= 0,V9 = V43,V44 >= 0,V = V42,V1 = V44,V43 >= 0,V41 >= 0]). eq(length(V, Out),0,[],[Out = 0,V45 >= 0,V = V45]). eq(plus(V, V1, Out),0,[],[Out = 0,V46 >= 0,V47 >= 0,V = V46,V1 = V47]). eq(ge(V, V1, Out),0,[],[Out = 0,V48 >= 0,V49 >= 0,V = V48,V1 = V49]). eq(if(V, V1, V9, V10, V19, Out),0,[],[Out = 0,V10 = V50,V51 >= 0,V52 >= 0,V9 = V53,V54 >= 0,V = V51,V1 = V54,V19 = V52,V53 >= 0,V50 >= 0]). eq(helpc(V, V1, V9, Out),0,[],[Out = 0,V55 >= 0,V9 = V56,V57 >= 0,V = V55,V1 = V57,V56 >= 0]). input_output_vars(app(V,V1,Out),[V,V1],[Out]). input_output_vars(plus(V,V1,Out),[V,V1],[Out]). input_output_vars(length(V,Out),[V],[Out]). input_output_vars(helpa(V,V1,V9,V10,Out),[V,V1,V9,V10],[Out]). input_output_vars(ge(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V9,V10,V19,Out),[V,V1,V9,V10,V19],[Out]). input_output_vars(greater(V,V1,Out),[V,V1],[Out]). input_output_vars(smaller(V,V1,Out),[V,V1],[Out]). input_output_vars(helpc(V,V1,V9,Out),[V,V1,V9],[Out]). input_output_vars(helpb(V,V1,V9,V10,Out),[V,V1,V9,V10],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [ge/3]
1. non_recursive : [helpc/4]
2. recursive : [length/2]
3. non_recursive : [greater/3]
4. non_recursive : [smaller/3]
5. recursive : [helpa/5,helpb/5,if/6]
6. recursive : [plus/3]
7. non_recursive : [app/3]
8. non_recursive : [start/5]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into ge/3
1. SCC is partially evaluated into helpc/4
2. SCC is partially evaluated into length/2
3. SCC is partially evaluated into greater/3
4. SCC is partially evaluated into smaller/3
5. SCC is partially evaluated into helpa/5
6. SCC is partially evaluated into plus/3
7. SCC is partially evaluated into app/3
8. SCC is partially evaluated into start/5
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations ge/3
* CE 31 is refined into CE [35]
* CE 28 is refined into CE [36]
* CE 29 is refined into CE [37]
* CE 30 is refined into CE [38]
### Cost equations --> "Loop" of ge/3
* CEs [38] --> Loop 20
* CEs [35] --> Loop 21
* CEs [36] --> Loop 22
* CEs [37] --> Loop 23
### Ranking functions of CR ge(V,V1,Out)
* RF of phase [20]: [V,V1]
#### Partial ranking functions of CR ge(V,V1,Out)
* Partial RF of phase [20]:
- RF of loop [20:1]:
V
V1
### Specialization of cost equations helpc/4
* CE 34 is refined into CE [39]
* CE 32 is refined into CE [40]
* CE 33 is refined into CE [41]
### Cost equations --> "Loop" of helpc/4
* CEs [39] --> Loop 24
* CEs [40] --> Loop 25
* CEs [41] --> Loop 26
### Ranking functions of CR helpc(V,V1,V9,Out)
#### Partial ranking functions of CR helpc(V,V1,V9,Out)
### Specialization of cost equations length/2
* CE 25 is refined into CE [42]
* CE 27 is refined into CE [43]
* CE 26 is refined into CE [44]
### Cost equations --> "Loop" of length/2
* CEs [44] --> Loop 27
* CEs [42,43] --> Loop 28
### Ranking functions of CR length(V,Out)
* RF of phase [27]: [V]
#### Partial ranking functions of CR length(V,Out)
* Partial RF of phase [27]:
- RF of loop [27:1]:
V
### Specialization of cost equations greater/3
* CE 15 is refined into CE [45,46,47,48,49,50,51,52,53,54,55,56,57,58]
### Cost equations --> "Loop" of greater/3
* CEs [48,55] --> Loop 29
* CEs [45,51,57] --> Loop 30
* CEs [46,47,49,50,52,53,54,56,58] --> Loop 31
### Ranking functions of CR greater(V,V1,Out)
#### Partial ranking functions of CR greater(V,V1,Out)
### Specialization of cost equations smaller/3
* CE 16 is refined into CE [59,60,61,62,63,64,65,66,67,68,69,70,71,72]
### Cost equations --> "Loop" of smaller/3
* CEs [59,65,71] --> Loop 32
* CEs [62,69] --> Loop 33
* CEs [60,61,63,64,66,67,68,70,72] --> Loop 34
### Ranking functions of CR smaller(V,V1,Out)
#### Partial ranking functions of CR smaller(V,V1,Out)
### Specialization of cost equations helpa/5
* CE 17 is refined into CE [73,74,75,76,77]
* CE 18 is refined into CE [78,79]
* CE 20 is refined into CE [80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97]
* CE 19 is refined into CE [98,99,100,101,102,103,104,105,106,107,108,109]
### Cost equations --> "Loop" of helpa/5
* CEs [109] --> Loop 35
* CEs [106] --> Loop 36
* CEs [108] --> Loop 37
* CEs [105] --> Loop 38
* CEs [107] --> Loop 39
* CEs [104] --> Loop 40
* CEs [103] --> Loop 41
* CEs [100] --> Loop 42
* CEs [102] --> Loop 43
* CEs [99] --> Loop 44
* CEs [101] --> Loop 45
* CEs [98] --> Loop 46
* CEs [74,78] --> Loop 47
* CEs [73,75,76,77,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97] --> Loop 48
### Ranking functions of CR helpa(V,V1,V9,V10,Out)
* RF of phase [35,36,37,38,39,40]: [-V+V1]
#### Partial ranking functions of CR helpa(V,V1,V9,V10,Out)
* Partial RF of phase [35,36,37,38,39,40]:
- RF of loop [35:1,36:1,37:1,38:1,39:1,40:1]:
-V+V1
- RF of loop [36:1,38:1,40:1]:
V9 depends on loops [35:1,37:1,39:1]
- RF of loop [37:1,39:1]:
V9+V10 depends on loops [35:1,38:1]
- RF of loop [39:1]:
V10 depends on loops [37:1,38:1]
### Specialization of cost equations plus/3
* CE 24 is refined into CE [110]
* CE 22 is refined into CE [111]
* CE 23 is refined into CE [112]
### Cost equations --> "Loop" of plus/3
* CEs [112] --> Loop 49
* CEs [110] --> Loop 50
* CEs [111] --> Loop 51
### Ranking functions of CR plus(V,V1,Out)
* RF of phase [49]: [V1]
#### Partial ranking functions of CR plus(V,V1,Out)
* Partial RF of phase [49]:
- RF of loop [49:1]:
V1
### Specialization of cost equations app/3
* CE 21 is refined into CE [113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142]
### Cost equations --> "Loop" of app/3
* CEs [117,122,127,134,139] --> Loop 52
* CEs [129] --> Loop 53
* CEs [128,135,136] --> Loop 54
* CEs [116,121,126,133,138] --> Loop 55
* CEs [118,119,123,124,140,141] --> Loop 56
* CEs [113,114,115,120,125,130,131,132,137,142] --> Loop 57
### Ranking functions of CR app(V,V1,Out)
#### Partial ranking functions of CR app(V,V1,Out)
### Specialization of cost equations start/5
* CE 3 is refined into CE [143]
* CE 2 is refined into CE [144]
* CE 4 is refined into CE [145,146,147,148,149,150,151,152,153,154,155,156]
* CE 5 is refined into CE [157,158,159,160,161,162,163,164,165]
* CE 6 is refined into CE [166,167]
* CE 7 is refined into CE [168,169,170,171,172,173]
* CE 8 is refined into CE [174,175,176,177]
* CE 9 is refined into CE [178,179]
* CE 10 is refined into CE [180,181,182,183,184,185]
* CE 11 is refined into CE [186,187,188,189,190]
* CE 12 is refined into CE [191,192,193]
* CE 13 is refined into CE [194,195,196]
* CE 14 is refined into CE [197,198,199]
### Cost equations --> "Loop" of start/5
* CEs [174,187] --> Loop 58
* CEs [143,198] --> Loop 59
* CEs [145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,197] --> Loop 60
* CEs [144,166,167,168,169,170,171,172,173,175,176,177,178,179,180,181,182,183,184,185,186,188,189,190,191,192,193,194,195,196,199] --> Loop 61
### Ranking functions of CR start(V,V1,V9,V10,V19)
#### Partial ranking functions of CR start(V,V1,V9,V10,V19)
Computing Bounds
=====================================
#### Cost of chains of ge(V,V1,Out):
* Chain [[20],23]: 1*it(20)+1
Such that:it(20) =< V
with precondition: [Out=1,V>=1,V1>=V+1]
* Chain [[20],22]: 1*it(20)+1
Such that:it(20) =< V1
with precondition: [Out=2,V1>=1,V>=V1]
* Chain [[20],21]: 1*it(20)+0
Such that:it(20) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [23]: 1
with precondition: [V=0,Out=1,V1>=1]
* Chain [22]: 1
with precondition: [V1=0,Out=2,V>=0]
* Chain [21]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of helpc(V,V1,V9,Out):
* Chain [26]: 1
with precondition: [V=1,V9=Out,V1>=0,V9>=0]
* Chain [25]: 1
with precondition: [V=2,V1=Out,V1>=0,V9>=0]
* Chain [24]: 0
with precondition: [Out=0,V>=0,V1>=0,V9>=0]
#### Cost of chains of length(V,Out):
* Chain [[27],28]: 1*it(27)+1
Such that:it(27) =< V
with precondition: [Out>=1,V>=Out]
* Chain [28]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of greater(V,V1,Out):
* Chain [31]: 9*s(3)+5*s(6)+4
Such that:aux(5) =< V
aux(6) =< V1
s(6) =< aux(5)
s(3) =< aux(6)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [30]: 2*s(18)+2*s(20)+5
Such that:aux(7) =< V1
aux(8) =< V
s(18) =< aux(8)
s(20) =< aux(7)
with precondition: [V=Out,V>=0,V1>=0]
* Chain [29]: 3*s(22)+1*s(23)+5
Such that:s(23) =< V
aux(10) =< V1
s(22) =< aux(10)
with precondition: [V1=Out,V>=0,V1>=1]
#### Cost of chains of smaller(V,V1,Out):
* Chain [34]: 9*s(27)+5*s(30)+4
Such that:aux(15) =< V
aux(16) =< V1
s(30) =< aux(15)
s(27) =< aux(16)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [33]: 3*s(42)+1*s(43)+5
Such that:s(43) =< V
aux(18) =< V1
s(42) =< aux(18)
with precondition: [V=Out,V>=0,V1>=1]
* Chain [32]: 2*s(46)+2*s(48)+5
Such that:aux(19) =< V1
aux(20) =< V
s(46) =< aux(20)
s(48) =< aux(19)
with precondition: [V1=Out,V>=0,V1>=0]
#### Cost of chains of helpa(V,V1,V9,V10,Out):
* Chain [[35,36,37,38,39,40],48]: 69*it(35)+13*it(39)+13*s(50)+264*s(56)+1*s(274)+8*s(275)+4*s(279)+31*s(280)+1*s(294)+6*s(295)+12*s(296)+11*s(301)+13
Such that:aux(118) =< V+V9+V10
aux(143) =< V1+2*V9+2*V10
aux(149) =< -V+V1
aux(150) =< V1
aux(151) =< V9+V10
aux(152) =< V10
s(50) =< aux(150)
s(56) =< aux(151)
it(35) =< aux(149)
it(39) =< aux(149)
aux(87) =< aux(151)
aux(86) =< aux(150)
aux(113) =< aux(151)-1
aux(116) =< it(35)*aux(143)
aux(77) =< it(35)*aux(151)
s(274) =< it(35)*aux(150)
aux(126) =< it(35)*aux(87)
s(279) =< it(35)*aux(86)
aux(105) =< it(35)*aux(113)
s(297) =< aux(105)+aux(77)+aux(152)
s(302) =< aux(105)+aux(77)+aux(152)
s(298) =< aux(116)+aux(116)+aux(118)
s(302) =< aux(116)+aux(116)+aux(118)
it(39) =< aux(105)+aux(77)+aux(152)
s(297) =< it(39)*aux(87)
s(298) =< it(39)*aux(87)
s(294) =< it(39)*aux(86)
s(280) =< aux(126)
s(301) =< s(302)
s(295) =< s(298)
s(296) =< s(297)
s(275) =< aux(77)
with precondition: [V>=1,V9>=0,V10>=0,Out>=1,V1>=V+1,V9+V10>=1]
* Chain [48]: 3*s(50)+10*s(51)+96*s(56)+168*s(57)+13
Such that:aux(57) =< V
aux(58) =< V1
aux(59) =< V9
aux(60) =< V10
s(51) =< aux(57)
s(50) =< aux(58)
s(56) =< aux(59)
s(57) =< aux(60)
with precondition: [Out=0,V>=0,V1>=0,V9>=0,V10>=0]
* Chain [47]: 3
with precondition: [V1=0,Out=0,V>=0,V9>=0,V10>=0]
* Chain [46,[35,36,37,38,39,40],48]: 82*it(35)+13*it(39)+271*s(56)+1*s(274)+8*s(275)+4*s(279)+31*s(280)+1*s(294)+6*s(295)+12*s(296)+11*s(301)+11*s(307)+26
Such that:aux(143) =< V1+2*V9
aux(154) =< V10
aux(155) =< V1
aux(156) =< V9
it(35) =< aux(155)
s(56) =< aux(156)
it(39) =< aux(155)
aux(87) =< aux(156)
aux(86) =< aux(155)
aux(113) =< aux(156)-1
aux(116) =< it(35)*aux(143)
aux(77) =< it(35)*aux(156)
s(274) =< it(35)*aux(155)
aux(126) =< it(35)*aux(87)
s(279) =< it(35)*aux(86)
aux(105) =< it(35)*aux(113)
s(297) =< aux(105)+aux(77)
s(302) =< aux(105)+aux(77)
s(298) =< aux(116)+aux(116)+aux(156)
s(302) =< aux(116)+aux(116)+aux(156)
it(39) =< aux(105)+aux(77)
s(297) =< it(39)*aux(87)
s(298) =< it(39)*aux(87)
s(294) =< it(39)*aux(86)
s(280) =< aux(126)
s(301) =< s(302)
s(295) =< s(298)
s(296) =< s(297)
s(275) =< aux(77)
s(307) =< aux(154)
with precondition: [V=0,V1>=2,V9>=2,V10>=0,Out>=2]
* Chain [46,48]: 3*s(50)+10*s(51)+96*s(56)+7*s(306)+11*s(307)+26
Such that:aux(57) =< 1
aux(58) =< V1
aux(153) =< V9
aux(59) =< V9-Out
aux(154) =< V10
s(51) =< aux(57)
s(50) =< aux(58)
s(56) =< aux(59)
s(306) =< aux(153)
s(307) =< aux(154)
with precondition: [V=0,V1>=1,V10>=0,Out>=1,V9>=Out]
* Chain [45,[35,36,37,38,39,40],48]: 82*it(35)+13*it(39)+276*s(56)+1*s(274)+8*s(275)+4*s(279)+31*s(280)+1*s(294)+6*s(295)+12*s(296)+11*s(301)+6*s(312)+26
Such that:aux(143) =< V1+2*V10
aux(157) =< V9
aux(159) =< V1
aux(160) =< V10
it(35) =< aux(159)
s(56) =< aux(160)
it(39) =< aux(159)
aux(87) =< aux(160)
aux(86) =< aux(159)
aux(113) =< aux(160)-1
aux(116) =< it(35)*aux(143)
aux(77) =< it(35)*aux(160)
s(274) =< it(35)*aux(159)
aux(126) =< it(35)*aux(87)
s(279) =< it(35)*aux(86)
aux(105) =< it(35)*aux(113)
s(297) =< aux(105)+aux(77)
s(302) =< aux(105)+aux(77)
s(298) =< aux(116)+aux(116)+aux(160)
s(302) =< aux(116)+aux(116)+aux(160)
it(39) =< aux(105)+aux(77)
s(297) =< it(39)*aux(87)
s(298) =< it(39)*aux(87)
s(294) =< it(39)*aux(86)
s(280) =< aux(126)
s(301) =< s(302)
s(295) =< s(298)
s(296) =< s(297)
s(275) =< aux(77)
s(312) =< aux(157)
with precondition: [V=0,V1>=2,V9>=0,V10>=2,Out>=2]
* Chain [45,48]: 3*s(50)+10*s(51)+96*s(56)+6*s(312)+12*s(314)+26
Such that:aux(57) =< 1
aux(58) =< V1
aux(157) =< V9
aux(158) =< V10
aux(59) =< V10-Out
s(51) =< aux(57)
s(50) =< aux(58)
s(56) =< aux(59)
s(312) =< aux(157)
s(314) =< aux(158)
with precondition: [V=0,V1>=1,V9>=0,Out>=1,V10>=Out]
* Chain [44,[35,36,37,38,39,40],48]: 82*it(35)+13*it(39)+264*s(56)+1*s(274)+8*s(275)+4*s(279)+31*s(280)+1*s(294)+6*s(295)+12*s(296)+11*s(301)+3*s(321)+5*s(322)+27
Such that:aux(143) =< V1+4*V9
aux(161) =< V10
aux(163) =< V1
aux(164) =< V9
aux(165) =< 2*V9
it(35) =< aux(163)
s(56) =< aux(165)
it(39) =< aux(163)
aux(87) =< aux(165)
aux(86) =< aux(163)
aux(113) =< aux(165)-1
aux(116) =< it(35)*aux(143)
aux(77) =< it(35)*aux(165)
s(274) =< it(35)*aux(163)
aux(126) =< it(35)*aux(87)
s(279) =< it(35)*aux(86)
aux(105) =< it(35)*aux(113)
s(297) =< aux(105)+aux(77)+aux(164)
s(302) =< aux(105)+aux(77)+aux(164)
s(298) =< aux(116)+aux(116)+aux(165)
s(302) =< aux(116)+aux(116)+aux(165)
it(39) =< aux(105)+aux(77)+aux(164)
s(297) =< it(39)*aux(87)
s(298) =< it(39)*aux(87)
s(294) =< it(39)*aux(86)
s(280) =< aux(126)
s(301) =< s(302)
s(295) =< s(298)
s(296) =< s(297)
s(275) =< aux(77)
s(321) =< aux(164)
s(322) =< aux(161)
with precondition: [V=0,V1>=2,V9>=1,V10>=1,Out>=2]
* Chain [44,48]: 3*s(50)+10*s(51)+96*s(56)+171*s(57)+5*s(322)+27
Such that:aux(57) =< 1
aux(58) =< V1
aux(59) =< V9-Out
aux(161) =< V10
aux(166) =< V9
s(51) =< aux(57)
s(50) =< aux(58)
s(56) =< aux(59)
s(57) =< aux(166)
s(322) =< aux(161)
with precondition: [V=0,V1>=1,V10>=1,Out>=1,V9>=Out]
* Chain [43,[35,36,37,38,39,40],48]: 82*it(35)+13*it(39)+264*s(56)+1*s(274)+8*s(275)+4*s(279)+31*s(280)+1*s(294)+6*s(295)+12*s(296)+11*s(301)+2*s(326)+6*s(328)+27
Such that:aux(143) =< V1+2*V9+2*V10
aux(167) =< V10
aux(169) =< V1
aux(170) =< V9
aux(171) =< V9+V10
it(35) =< aux(169)
s(56) =< aux(171)
it(39) =< aux(169)
aux(87) =< aux(171)
aux(86) =< aux(169)
aux(113) =< aux(171)-1
aux(116) =< it(35)*aux(143)
aux(77) =< it(35)*aux(171)
s(274) =< it(35)*aux(169)
aux(126) =< it(35)*aux(87)
s(279) =< it(35)*aux(86)
aux(105) =< it(35)*aux(113)
s(297) =< aux(105)+aux(77)+aux(170)
s(302) =< aux(105)+aux(77)+aux(170)
s(298) =< aux(116)+aux(116)+aux(171)
s(302) =< aux(116)+aux(116)+aux(171)
it(39) =< aux(105)+aux(77)+aux(170)
s(297) =< it(39)*aux(87)
s(298) =< it(39)*aux(87)
s(294) =< it(39)*aux(86)
s(280) =< aux(126)
s(301) =< s(302)
s(295) =< s(298)
s(296) =< s(297)
s(275) =< aux(77)
s(326) =< aux(170)
s(328) =< aux(167)
with precondition: [V=0,V1>=2,V9>=0,V10>=1,Out>=2,V9+V10>=2]
* Chain [43,48]: 3*s(50)+10*s(51)+96*s(56)+170*s(57)+6*s(328)+27
Such that:aux(57) =< 1
aux(58) =< V1
aux(167) =< V10
aux(59) =< V10-Out
aux(172) =< V9
s(51) =< aux(57)
s(50) =< aux(58)
s(56) =< aux(59)
s(57) =< aux(172)
s(328) =< aux(167)
with precondition: [V=0,V1>=1,V9>=0,Out>=1,V10>=Out]
* Chain [42,[35,36,37,38,39,40],48]: 82*it(35)+13*it(39)+264*s(56)+1*s(274)+8*s(275)+4*s(279)+31*s(280)+1*s(294)+6*s(295)+12*s(296)+11*s(301)+4*s(334)+4*s(335)+27
Such that:aux(143) =< V1+2*V9+2*V10
aux(173) =< V9
aux(175) =< V1
aux(176) =< V9+V10
aux(177) =< V10
it(35) =< aux(175)
s(56) =< aux(176)
it(39) =< aux(175)
aux(87) =< aux(176)
aux(86) =< aux(175)
aux(113) =< aux(176)-1
aux(116) =< it(35)*aux(143)
aux(77) =< it(35)*aux(176)
s(274) =< it(35)*aux(175)
aux(126) =< it(35)*aux(87)
s(279) =< it(35)*aux(86)
aux(105) =< it(35)*aux(113)
s(297) =< aux(105)+aux(77)+aux(177)
s(302) =< aux(105)+aux(77)+aux(177)
s(298) =< aux(116)+aux(116)+aux(176)
s(302) =< aux(116)+aux(116)+aux(176)
it(39) =< aux(105)+aux(77)+aux(177)
s(297) =< it(39)*aux(87)
s(298) =< it(39)*aux(87)
s(294) =< it(39)*aux(86)
s(280) =< aux(126)
s(301) =< s(302)
s(295) =< s(298)
s(296) =< s(297)
s(275) =< aux(77)
s(334) =< aux(173)
s(335) =< aux(177)
with precondition: [V=0,V1>=2,V9>=1,V10>=0,Out>=2,V9+V10>=2]
* Chain [42,48]: 3*s(50)+10*s(51)+96*s(56)+172*s(57)+4*s(334)+27
Such that:aux(57) =< 1
aux(58) =< V1
aux(173) =< V9
aux(59) =< V9-Out
aux(178) =< V10
s(51) =< aux(57)
s(50) =< aux(58)
s(56) =< aux(59)
s(57) =< aux(178)
s(334) =< aux(173)
with precondition: [V=0,V1>=1,V10>=0,Out>=1,V9>=Out]
* Chain [41,[35,36,37,38,39,40],48]: 82*it(35)+13*it(39)+264*s(56)+1*s(274)+8*s(275)+4*s(279)+31*s(280)+1*s(294)+6*s(295)+12*s(296)+11*s(301)+3*s(340)+5*s(342)+27
Such that:aux(143) =< V1+4*V10
aux(179) =< V9
aux(181) =< V1
aux(182) =< V10
aux(183) =< 2*V10
it(35) =< aux(181)
s(56) =< aux(183)
it(39) =< aux(181)
aux(87) =< aux(183)
aux(86) =< aux(181)
aux(113) =< aux(183)-1
aux(116) =< it(35)*aux(143)
aux(77) =< it(35)*aux(183)
s(274) =< it(35)*aux(181)
aux(126) =< it(35)*aux(87)
s(279) =< it(35)*aux(86)
aux(105) =< it(35)*aux(113)
s(297) =< aux(105)+aux(77)+aux(182)
s(302) =< aux(105)+aux(77)+aux(182)
s(298) =< aux(116)+aux(116)+aux(183)
s(302) =< aux(116)+aux(116)+aux(183)
it(39) =< aux(105)+aux(77)+aux(182)
s(297) =< it(39)*aux(87)
s(298) =< it(39)*aux(87)
s(294) =< it(39)*aux(86)
s(280) =< aux(126)
s(301) =< s(302)
s(295) =< s(298)
s(296) =< s(297)
s(275) =< aux(77)
s(340) =< aux(179)
s(342) =< aux(182)
with precondition: [V=0,V1>=2,V9>=0,V10>=1,Out>=2]
* Chain [41,48]: 3*s(50)+10*s(51)+96*s(56)+173*s(57)+3*s(340)+27
Such that:aux(57) =< 1
aux(58) =< V1
aux(179) =< V9
aux(59) =< V10-Out
aux(184) =< V10
s(51) =< aux(57)
s(50) =< aux(58)
s(56) =< aux(59)
s(57) =< aux(184)
s(340) =< aux(179)
with precondition: [V=0,V1>=1,V9>=0,Out>=1,V10>=Out]
#### Cost of chains of plus(V,V1,Out):
* Chain [[49],51]: 1*it(49)+1
Such that:it(49) =< V1
with precondition: [V+V1=Out,V>=0,V1>=1]
* Chain [[49],50]: 1*it(49)+0
Such that:it(49) =< Out
with precondition: [V>=0,Out>=1,V1>=Out]
* Chain [51]: 1
with precondition: [V1=0,V=Out,V>=0]
* Chain [50]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of app(V,V1,Out):
* Chain [57]: 968*s(585)+1699*s(586)+3*s(660)+17
Such that:s(656) =< V+V1
aux(217) =< V
aux(218) =< V1
s(585) =< aux(217)
s(586) =< aux(218)
s(660) =< s(656)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [56]: 2409*s(674)+1584*s(687)+39*s(688)+18*s(694)+72*s(696)+3*s(701)+186*s(702)+33*s(703)+18*s(704)+36*s(705)+48*s(706)+869*s(707)+792*s(709)+39*s(710)+3*s(720)+93*s(721)+33*s(722)+18*s(723)+36*s(724)+24*s(725)+39*s(726)+3*s(736)+93*s(737)+33*s(738)+18*s(739)+36*s(740)+24*s(741)+792*s(742)+39*s(743)+3*s(753)+93*s(754)+33*s(755)+18*s(756)+36*s(757)+24*s(758)+39*s(769)+3*s(782)+93*s(783)+33*s(784)+18*s(785)+36*s(786)+24*s(787)+39*s(790)+3*s(800)+33*s(802)+18*s(803)+36*s(804)+31
Such that:aux(227) =< V
aux(228) =< V+V1
aux(229) =< 2*V
aux(230) =< 2*V+V1
aux(231) =< 2*V+3*V1
aux(232) =< 4*V+V1
aux(233) =< V1
aux(234) =< 2*V1
aux(235) =< 3*V1
aux(236) =< 5*V1
s(674) =< aux(233)
s(687) =< aux(228)
s(688) =< aux(233)
s(689) =< aux(228)
s(690) =< aux(233)
s(691) =< aux(228)-1
s(692) =< s(674)*aux(231)
s(693) =< s(674)*aux(228)
s(694) =< s(674)*aux(233)
s(695) =< s(674)*s(689)
s(696) =< s(674)*s(690)
s(697) =< s(674)*s(691)
s(698) =< s(697)+s(693)+aux(227)
s(699) =< s(697)+s(693)+aux(227)
s(700) =< s(692)+s(692)+aux(228)
s(699) =< s(692)+s(692)+aux(228)
s(688) =< s(697)+s(693)+aux(227)
s(698) =< s(688)*s(689)
s(700) =< s(688)*s(689)
s(701) =< s(688)*s(690)
s(702) =< s(695)
s(703) =< s(699)
s(704) =< s(700)
s(705) =< s(698)
s(706) =< s(693)
s(707) =< aux(227)
s(709) =< aux(229)
s(710) =< aux(233)
s(711) =< aux(229)
s(712) =< aux(229)-1
s(713) =< s(674)*aux(232)
s(714) =< s(674)*aux(229)
s(715) =< s(674)*s(711)
s(716) =< s(674)*s(712)
s(717) =< s(716)+s(714)+aux(227)
s(718) =< s(716)+s(714)+aux(227)
s(719) =< s(713)+s(713)+aux(229)
s(718) =< s(713)+s(713)+aux(229)
s(710) =< s(716)+s(714)+aux(227)
s(717) =< s(710)*s(711)
s(719) =< s(710)*s(711)
s(720) =< s(710)*s(690)
s(721) =< s(715)
s(722) =< s(718)
s(723) =< s(719)
s(724) =< s(717)
s(725) =< s(714)
s(726) =< aux(233)
s(728) =< aux(233)-1
s(729) =< s(674)*aux(235)
s(730) =< s(674)*aux(233)
s(731) =< s(674)*s(690)
s(732) =< s(674)*s(728)
s(733) =< s(732)+s(730)
s(734) =< s(732)+s(730)
s(735) =< s(729)+s(729)+aux(233)
s(734) =< s(729)+s(729)+aux(233)
s(726) =< s(732)+s(730)
s(733) =< s(726)*s(690)
s(735) =< s(726)*s(690)
s(736) =< s(726)*s(690)
s(737) =< s(731)
s(738) =< s(734)
s(739) =< s(735)
s(740) =< s(733)
s(741) =< s(730)
s(742) =< aux(234)
s(743) =< aux(233)
s(744) =< aux(234)
s(745) =< aux(234)-1
s(746) =< s(674)*aux(236)
s(747) =< s(674)*aux(234)
s(748) =< s(674)*s(744)
s(749) =< s(674)*s(745)
s(750) =< s(749)+s(747)+aux(233)
s(751) =< s(749)+s(747)+aux(233)
s(752) =< s(746)+s(746)+aux(234)
s(751) =< s(746)+s(746)+aux(234)
s(743) =< s(749)+s(747)+aux(233)
s(750) =< s(743)*s(744)
s(752) =< s(743)*s(744)
s(753) =< s(743)*s(690)
s(754) =< s(748)
s(755) =< s(751)
s(756) =< s(752)
s(757) =< s(750)
s(758) =< s(747)
s(769) =< aux(233)
s(770) =< aux(227)
s(772) =< aux(227)-1
s(773) =< s(674)*aux(230)
s(774) =< s(674)*aux(227)
s(776) =< s(674)*s(770)
s(778) =< s(674)*s(772)
s(779) =< s(778)+s(774)
s(780) =< s(778)+s(774)
s(781) =< s(773)+s(773)+aux(227)
s(780) =< s(773)+s(773)+aux(227)
s(769) =< s(778)+s(774)
s(779) =< s(769)*s(770)
s(781) =< s(769)*s(770)
s(782) =< s(769)*s(690)
s(783) =< s(776)
s(784) =< s(780)
s(785) =< s(781)
s(786) =< s(779)
s(787) =< s(774)
s(790) =< aux(233)
s(797) =< s(697)+s(693)+aux(233)
s(798) =< s(697)+s(693)+aux(233)
s(799) =< s(692)+s(692)+aux(228)
s(798) =< s(692)+s(692)+aux(228)
s(790) =< s(697)+s(693)+aux(233)
s(797) =< s(790)*s(689)
s(799) =< s(790)*s(689)
s(800) =< s(790)*s(690)
s(802) =< s(798)
s(803) =< s(799)
s(804) =< s(797)
with precondition: [V>=0,V1>=2,Out>=2]
* Chain [55]: 2430*s(1072)+150*s(1079)+907*s(1083)+9*s(1116)+31
Such that:s(1111) =< V+V1
aux(245) =< 1
aux(246) =< V
aux(247) =< V1
s(1072) =< aux(247)
s(1079) =< aux(245)
s(1083) =< aux(246)
s(1116) =< s(1111)
with precondition: [V>=0,Out>=1,V1>=Out]
* Chain [54]: 634*s(1133)+1284*s(1145)+13*s(1146)+4*s(1152)+16*s(1154)+1*s(1159)+31*s(1160)+11*s(1161)+6*s(1162)+12*s(1163)+8*s(1164)+603*s(1166)+528*s(1167)+13*s(1168)+1*s(1178)+31*s(1179)+11*s(1180)+6*s(1181)+12*s(1182)+8*s(1183)+13*s(1184)+1*s(1194)+31*s(1195)+11*s(1196)+6*s(1197)+12*s(1198)+8*s(1199)+528*s(1200)+13*s(1201)+1*s(1211)+31*s(1212)+11*s(1213)+6*s(1214)+12*s(1215)+8*s(1216)+13*s(1232)+6*s(1238)+24*s(1240)+1*s(1245)+62*s(1246)+11*s(1247)+6*s(1248)+12*s(1249)+16*s(1250)+13*s(1254)+1*s(1264)+31*s(1265)+11*s(1266)+6*s(1267)+12*s(1268)+8*s(1269)+13*s(1270)+1*s(1280)+31*s(1281)+11*s(1282)+6*s(1283)+12*s(1284)+8*s(1285)+13*s(1287)+1*s(1297)+31*s(1298)+11*s(1299)+6*s(1300)+12*s(1301)+8*s(1302)+13*s(1314)+1*s(1327)+31*s(1328)+11*s(1329)+6*s(1330)+12*s(1331)+8*s(1332)+13*s(1335)+1*s(1345)+11*s(1347)+6*s(1348)+12*s(1349)+31
Such that:s(1136) =< V+2*V1
s(1222) =< V+3*V1
s(1137) =< V+4*V1
s(1223) =< V+5*V1
s(1306) =< 3*V+V1
s(1134) =< 3*V+2*V1
s(1135) =< 5*V
s(1221) =< 5*V+V1
aux(255) =< V
aux(256) =< V+V1
aux(257) =< 2*V
aux(258) =< 3*V+3*V1
aux(259) =< V1
aux(260) =< 2*V1
s(1133) =< aux(255)
s(1145) =< aux(256)
s(1146) =< aux(255)
s(1147) =< aux(256)
s(1148) =< aux(255)
s(1149) =< aux(256)-1
s(1150) =< s(1133)*s(1134)
s(1151) =< s(1133)*aux(256)
s(1152) =< s(1133)*aux(255)
s(1153) =< s(1133)*s(1147)
s(1154) =< s(1133)*s(1148)
s(1155) =< s(1133)*s(1149)
s(1156) =< s(1155)+s(1151)+aux(255)
s(1157) =< s(1155)+s(1151)+aux(255)
s(1158) =< s(1150)+s(1150)+aux(256)
s(1157) =< s(1150)+s(1150)+aux(256)
s(1146) =< s(1155)+s(1151)+aux(255)
s(1156) =< s(1146)*s(1147)
s(1158) =< s(1146)*s(1147)
s(1159) =< s(1146)*s(1148)
s(1160) =< s(1153)
s(1161) =< s(1157)
s(1162) =< s(1158)
s(1163) =< s(1156)
s(1164) =< s(1151)
s(1166) =< aux(259)
s(1167) =< aux(257)
s(1168) =< aux(255)
s(1169) =< aux(257)
s(1170) =< aux(257)-1
s(1171) =< s(1133)*s(1135)
s(1172) =< s(1133)*aux(257)
s(1173) =< s(1133)*s(1169)
s(1174) =< s(1133)*s(1170)
s(1175) =< s(1174)+s(1172)+aux(255)
s(1176) =< s(1174)+s(1172)+aux(255)
s(1177) =< s(1171)+s(1171)+aux(257)
s(1176) =< s(1171)+s(1171)+aux(257)
s(1168) =< s(1174)+s(1172)+aux(255)
s(1175) =< s(1168)*s(1169)
s(1177) =< s(1168)*s(1169)
s(1178) =< s(1168)*s(1148)
s(1179) =< s(1173)
s(1180) =< s(1176)
s(1181) =< s(1177)
s(1182) =< s(1175)
s(1183) =< s(1172)
s(1184) =< aux(255)
s(1185) =< aux(259)
s(1186) =< aux(259)-1
s(1187) =< s(1133)*s(1136)
s(1188) =< s(1133)*aux(259)
s(1189) =< s(1133)*s(1185)
s(1190) =< s(1133)*s(1186)
s(1191) =< s(1190)+s(1188)
s(1192) =< s(1190)+s(1188)
s(1193) =< s(1187)+s(1187)+aux(259)
s(1192) =< s(1187)+s(1187)+aux(259)
s(1184) =< s(1190)+s(1188)
s(1191) =< s(1184)*s(1185)
s(1193) =< s(1184)*s(1185)
s(1194) =< s(1184)*s(1148)
s(1195) =< s(1189)
s(1196) =< s(1192)
s(1197) =< s(1193)
s(1198) =< s(1191)
s(1199) =< s(1188)
s(1200) =< aux(260)
s(1201) =< aux(255)
s(1202) =< aux(260)
s(1203) =< aux(260)-1
s(1204) =< s(1133)*s(1137)
s(1205) =< s(1133)*aux(260)
s(1206) =< s(1133)*s(1202)
s(1207) =< s(1133)*s(1203)
s(1208) =< s(1207)+s(1205)+aux(259)
s(1209) =< s(1207)+s(1205)+aux(259)
s(1210) =< s(1204)+s(1204)+aux(260)
s(1209) =< s(1204)+s(1204)+aux(260)
s(1201) =< s(1207)+s(1205)+aux(259)
s(1208) =< s(1201)*s(1202)
s(1210) =< s(1201)*s(1202)
s(1211) =< s(1201)*s(1148)
s(1212) =< s(1206)
s(1213) =< s(1209)
s(1214) =< s(1210)
s(1215) =< s(1208)
s(1216) =< s(1205)
s(1232) =< aux(256)
s(1236) =< s(1145)*aux(258)
s(1237) =< s(1145)*aux(256)
s(1238) =< s(1145)*aux(256)
s(1239) =< s(1145)*s(1147)
s(1240) =< s(1145)*s(1147)
s(1241) =< s(1145)*s(1149)
s(1242) =< s(1241)+s(1237)+aux(255)
s(1243) =< s(1241)+s(1237)+aux(255)
s(1244) =< s(1236)+s(1236)+aux(256)
s(1243) =< s(1236)+s(1236)+aux(256)
s(1232) =< s(1241)+s(1237)+aux(255)
s(1242) =< s(1232)*s(1147)
s(1244) =< s(1232)*s(1147)
s(1245) =< s(1232)*s(1147)
s(1246) =< s(1239)
s(1247) =< s(1243)
s(1248) =< s(1244)
s(1249) =< s(1242)
s(1250) =< s(1237)
s(1254) =< aux(256)
s(1257) =< s(1145)*s(1221)
s(1258) =< s(1145)*aux(257)
s(1259) =< s(1145)*s(1169)
s(1260) =< s(1145)*s(1170)
s(1261) =< s(1260)+s(1258)+aux(255)
s(1262) =< s(1260)+s(1258)+aux(255)
s(1263) =< s(1257)+s(1257)+aux(257)
s(1262) =< s(1257)+s(1257)+aux(257)
s(1254) =< s(1260)+s(1258)+aux(255)
s(1261) =< s(1254)*s(1169)
s(1263) =< s(1254)*s(1169)
s(1264) =< s(1254)*s(1147)
s(1265) =< s(1259)
s(1266) =< s(1262)
s(1267) =< s(1263)
s(1268) =< s(1261)
s(1269) =< s(1258)
s(1270) =< aux(256)
s(1273) =< s(1145)*s(1222)
s(1274) =< s(1145)*aux(259)
s(1275) =< s(1145)*s(1185)
s(1276) =< s(1145)*s(1186)
s(1277) =< s(1276)+s(1274)
s(1278) =< s(1276)+s(1274)
s(1279) =< s(1273)+s(1273)+aux(259)
s(1278) =< s(1273)+s(1273)+aux(259)
s(1270) =< s(1276)+s(1274)
s(1277) =< s(1270)*s(1185)
s(1279) =< s(1270)*s(1185)
s(1280) =< s(1270)*s(1147)
s(1281) =< s(1275)
s(1282) =< s(1278)
s(1283) =< s(1279)
s(1284) =< s(1277)
s(1285) =< s(1274)
s(1287) =< aux(256)
s(1290) =< s(1145)*s(1223)
s(1291) =< s(1145)*aux(260)
s(1292) =< s(1145)*s(1202)
s(1293) =< s(1145)*s(1203)
s(1294) =< s(1293)+s(1291)+aux(259)
s(1295) =< s(1293)+s(1291)+aux(259)
s(1296) =< s(1290)+s(1290)+aux(260)
s(1295) =< s(1290)+s(1290)+aux(260)
s(1287) =< s(1293)+s(1291)+aux(259)
s(1294) =< s(1287)*s(1202)
s(1296) =< s(1287)*s(1202)
s(1297) =< s(1287)*s(1147)
s(1298) =< s(1292)
s(1299) =< s(1295)
s(1300) =< s(1296)
s(1301) =< s(1294)
s(1302) =< s(1291)
s(1314) =< aux(256)
s(1317) =< aux(255)-1
s(1318) =< s(1145)*s(1306)
s(1319) =< s(1145)*aux(255)
s(1321) =< s(1145)*s(1148)
s(1323) =< s(1145)*s(1317)
s(1324) =< s(1323)+s(1319)
s(1325) =< s(1323)+s(1319)
s(1326) =< s(1318)+s(1318)+aux(255)
s(1325) =< s(1318)+s(1318)+aux(255)
s(1314) =< s(1323)+s(1319)
s(1324) =< s(1314)*s(1148)
s(1326) =< s(1314)*s(1148)
s(1327) =< s(1314)*s(1147)
s(1328) =< s(1321)
s(1329) =< s(1325)
s(1330) =< s(1326)
s(1331) =< s(1324)
s(1332) =< s(1319)
s(1335) =< aux(256)
s(1342) =< s(1241)+s(1237)+aux(259)
s(1343) =< s(1241)+s(1237)+aux(259)
s(1344) =< s(1236)+s(1236)+aux(256)
s(1343) =< s(1236)+s(1236)+aux(256)
s(1335) =< s(1241)+s(1237)+aux(259)
s(1342) =< s(1335)*s(1147)
s(1344) =< s(1335)*s(1147)
s(1345) =< s(1335)*s(1147)
s(1347) =< s(1343)
s(1348) =< s(1344)
s(1349) =< s(1342)
with precondition: [V>=1,V1>=1,Out>=2]
* Chain [53]: 440*s(1351)+13*s(1360)+2*s(1366)+8*s(1368)+1*s(1373)+31*s(1374)+11*s(1375)+6*s(1376)+12*s(1377)+8*s(1378)+15*s(1379)+264*s(1380)+13*s(1381)+1*s(1391)+31*s(1392)+11*s(1393)+6*s(1394)+12*s(1395)+8*s(1396)+31
Such that:s(1354) =< V+V1
s(1352) =< 3*V
s(1353) =< 3*V+2*V1
s(1357) =< V1
aux(261) =< V
s(1351) =< aux(261)
s(1360) =< aux(261)
s(1361) =< aux(261)
s(1363) =< aux(261)-1
s(1364) =< s(1351)*s(1352)
s(1365) =< s(1351)*aux(261)
s(1366) =< s(1351)*aux(261)
s(1367) =< s(1351)*s(1361)
s(1368) =< s(1351)*s(1361)
s(1369) =< s(1351)*s(1363)
s(1370) =< s(1369)+s(1365)
s(1371) =< s(1369)+s(1365)
s(1372) =< s(1364)+s(1364)+aux(261)
s(1371) =< s(1364)+s(1364)+aux(261)
s(1360) =< s(1369)+s(1365)
s(1370) =< s(1360)*s(1361)
s(1372) =< s(1360)*s(1361)
s(1373) =< s(1360)*s(1361)
s(1374) =< s(1367)
s(1375) =< s(1371)
s(1376) =< s(1372)
s(1377) =< s(1370)
s(1378) =< s(1365)
s(1379) =< s(1357)
s(1380) =< s(1354)
s(1381) =< aux(261)
s(1382) =< s(1354)
s(1383) =< s(1354)-1
s(1384) =< s(1351)*s(1353)
s(1385) =< s(1351)*s(1354)
s(1386) =< s(1351)*s(1382)
s(1387) =< s(1351)*s(1383)
s(1388) =< s(1387)+s(1385)+s(1357)
s(1389) =< s(1387)+s(1385)+s(1357)
s(1390) =< s(1384)+s(1384)+s(1354)
s(1389) =< s(1384)+s(1384)+s(1354)
s(1381) =< s(1387)+s(1385)+s(1357)
s(1388) =< s(1381)*s(1382)
s(1390) =< s(1381)*s(1382)
s(1391) =< s(1381)*s(1361)
s(1392) =< s(1386)
s(1393) =< s(1389)
s(1394) =< s(1390)
s(1395) =< s(1388)
s(1396) =< s(1385)
with precondition: [V>=2,V1>=0,Out>=2]
* Chain [52]: 975*s(1397)+150*s(1404)+2362*s(1406)+9*s(1441)+31
Such that:s(1436) =< V+V1
aux(271) =< 1
aux(272) =< V
aux(273) =< V1
s(1397) =< aux(273)
s(1404) =< aux(271)
s(1406) =< aux(272)
s(1441) =< s(1436)
with precondition: [V1>=0,Out>=1,V>=Out]
#### Cost of chains of start(V,V1,V9,V10,V19):
* Chain [61]: 10*s(1462)+8705*s(1463)+1130*s(1464)+1310*s(1465)+1056*s(1473)+138*s(1474)+26*s(1475)+2*s(1481)+8*s(1483)+2*s(1488)+62*s(1489)+22*s(1490)+12*s(1491)+24*s(1492)+16*s(1493)+6208*s(1497)+3153*s(1499)+39*s(1512)+24*s(1518)+96*s(1520)+3*s(1525)+186*s(1526)+33*s(1527)+18*s(1528)+36*s(1529)+48*s(1530)+1320*s(1532)+39*s(1533)+3*s(1543)+93*s(1544)+33*s(1545)+18*s(1546)+36*s(1547)+24*s(1548)+39*s(1549)+3*s(1558)+93*s(1559)+33*s(1560)+18*s(1561)+36*s(1562)+24*s(1563)+1320*s(1564)+39*s(1565)+3*s(1575)+93*s(1576)+33*s(1577)+18*s(1578)+36*s(1579)+24*s(1580)+39*s(1581)+3*s(1591)+93*s(1592)+33*s(1593)+18*s(1594)+36*s(1595)+24*s(1596)+39*s(1597)+3*s(1601)+33*s(1602)+18*s(1603)+36*s(1604)+360*s(1610)+13*s(1629)+6*s(1635)+24*s(1637)+1*s(1642)+62*s(1643)+11*s(1644)+6*s(1645)+12*s(1646)+16*s(1647)+13*s(1650)+1*s(1660)+31*s(1661)+11*s(1662)+6*s(1663)+12*s(1664)+8*s(1665)+13*s(1666)+1*s(1676)+31*s(1677)+11*s(1678)+6*s(1679)+12*s(1680)+8*s(1681)+13*s(1683)+1*s(1693)+31*s(1694)+11*s(1695)+6*s(1696)+12*s(1697)+8*s(1698)+13*s(1699)+6*s(1702)+24*s(1704)+1*s(1709)+62*s(1710)+11*s(1711)+6*s(1712)+12*s(1713)+16*s(1714)+13*s(1715)+1*s(1723)+31*s(1724)+11*s(1725)+6*s(1726)+12*s(1727)+8*s(1728)+13*s(1729)+1*s(1737)+31*s(1738)+11*s(1739)+6*s(1740)+12*s(1741)+8*s(1742)+13*s(1743)+1*s(1751)+31*s(1752)+11*s(1753)+6*s(1754)+12*s(1755)+8*s(1756)+13*s(1757)+1*s(1766)+31*s(1767)+11*s(1768)+6*s(1769)+12*s(1770)+8*s(1771)+13*s(1772)+1*s(1776)+11*s(1777)+6*s(1778)+12*s(1779)+13*s(1786)+1*s(1798)+31*s(1799)+11*s(1800)+6*s(1801)+12*s(1802)+8*s(1803)+13*s(1806)+1*s(1816)+11*s(1818)+6*s(1819)+12*s(1820)+13*s(1865)+1*s(1878)+62*s(1879)+11*s(1880)+6*s(1881)+12*s(1882)+16*s(1883)+264*s(1886)+13*s(1887)+1*s(1897)+31*s(1898)+11*s(1899)+6*s(1900)+12*s(1901)+8*s(1902)+13*s(1903)+1*s(1913)+31*s(1914)+11*s(1915)+6*s(1916)+12*s(1917)+8*s(1918)+264*s(1919)+13*s(1920)+1*s(1930)+31*s(1931)+11*s(1932)+6*s(1933)+12*s(1934)+8*s(1935)+13*s(1944)+1*s(1957)+31*s(1958)+11*s(1959)+6*s(1960)+12*s(1961)+8*s(1962)+13*s(1965)+1*s(1975)+11*s(1977)+6*s(1978)+12*s(1979)+31
Such that:s(1458) =< V+1
s(1613) =< V+2*V1
s(1614) =< V+3*V1
s(1615) =< V+4*V1
s(1616) =< V+5*V1
s(1503) =< 2*V+V1
s(1504) =< 2*V+3*V1
s(1781) =< 3*V
s(1617) =< 3*V+V1
s(1624) =< 3*V+3*V1
s(1505) =< 4*V+V1
s(1619) =< 5*V
s(1620) =< 5*V+V1
s(1936) =< V1+2*V9
s(1854) =< V1+4*V9
s(1855) =< V1+2*V10
s(1856) =< V1+4*V10
s(1508) =< 3*V1
s(1509) =< 5*V1
s(1858) =< 2*V9
s(1859) =< 2*V10
aux(276) =< 1
aux(277) =< -V+V1
aux(278) =< V
aux(279) =< V+V1
aux(280) =< V+V9+V10
aux(281) =< 2*V
aux(282) =< 3*V+2*V1
aux(283) =< V1
aux(284) =< V1+2*V9+2*V10
aux(285) =< 2*V1
aux(286) =< V9
aux(287) =< V9+V10
aux(288) =< V10
s(1497) =< aux(278)
s(1463) =< aux(283)
s(1610) =< aux(276)
s(1499) =< aux(279)
s(1465) =< aux(288)
s(1464) =< aux(286)
s(1473) =< aux(287)
s(1474) =< aux(277)
s(1475) =< aux(277)
s(1476) =< aux(287)
s(1477) =< aux(283)
s(1478) =< aux(287)-1
s(1479) =< s(1474)*aux(284)
s(1480) =< s(1474)*aux(287)
s(1481) =< s(1474)*aux(283)
s(1482) =< s(1474)*s(1476)
s(1483) =< s(1474)*s(1477)
s(1484) =< s(1474)*s(1478)
s(1485) =< s(1484)+s(1480)+aux(288)
s(1486) =< s(1484)+s(1480)+aux(288)
s(1487) =< s(1479)+s(1479)+aux(280)
s(1486) =< s(1479)+s(1479)+aux(280)
s(1475) =< s(1484)+s(1480)+aux(288)
s(1485) =< s(1475)*s(1476)
s(1487) =< s(1475)*s(1476)
s(1488) =< s(1475)*s(1477)
s(1489) =< s(1482)
s(1490) =< s(1486)
s(1491) =< s(1487)
s(1492) =< s(1485)
s(1493) =< s(1480)
s(1512) =< aux(283)
s(1513) =< aux(279)
s(1515) =< aux(279)-1
s(1516) =< s(1463)*s(1504)
s(1517) =< s(1463)*aux(279)
s(1518) =< s(1463)*aux(283)
s(1519) =< s(1463)*s(1513)
s(1520) =< s(1463)*s(1477)
s(1521) =< s(1463)*s(1515)
s(1522) =< s(1521)+s(1517)+aux(278)
s(1523) =< s(1521)+s(1517)+aux(278)
s(1524) =< s(1516)+s(1516)+aux(279)
s(1523) =< s(1516)+s(1516)+aux(279)
s(1512) =< s(1521)+s(1517)+aux(278)
s(1522) =< s(1512)*s(1513)
s(1524) =< s(1512)*s(1513)
s(1525) =< s(1512)*s(1477)
s(1526) =< s(1519)
s(1527) =< s(1523)
s(1528) =< s(1524)
s(1529) =< s(1522)
s(1530) =< s(1517)
s(1532) =< aux(281)
s(1533) =< aux(283)
s(1534) =< aux(281)
s(1535) =< aux(281)-1
s(1536) =< s(1463)*s(1505)
s(1537) =< s(1463)*aux(281)
s(1538) =< s(1463)*s(1534)
s(1539) =< s(1463)*s(1535)
s(1540) =< s(1539)+s(1537)+aux(278)
s(1541) =< s(1539)+s(1537)+aux(278)
s(1542) =< s(1536)+s(1536)+aux(281)
s(1541) =< s(1536)+s(1536)+aux(281)
s(1533) =< s(1539)+s(1537)+aux(278)
s(1540) =< s(1533)*s(1534)
s(1542) =< s(1533)*s(1534)
s(1543) =< s(1533)*s(1477)
s(1544) =< s(1538)
s(1545) =< s(1541)
s(1546) =< s(1542)
s(1547) =< s(1540)
s(1548) =< s(1537)
s(1549) =< aux(283)
s(1550) =< aux(283)-1
s(1551) =< s(1463)*s(1508)
s(1552) =< s(1463)*aux(283)
s(1553) =< s(1463)*s(1477)
s(1554) =< s(1463)*s(1550)
s(1555) =< s(1554)+s(1552)
s(1556) =< s(1554)+s(1552)
s(1557) =< s(1551)+s(1551)+aux(283)
s(1556) =< s(1551)+s(1551)+aux(283)
s(1549) =< s(1554)+s(1552)
s(1555) =< s(1549)*s(1477)
s(1557) =< s(1549)*s(1477)
s(1558) =< s(1549)*s(1477)
s(1559) =< s(1553)
s(1560) =< s(1556)
s(1561) =< s(1557)
s(1562) =< s(1555)
s(1563) =< s(1552)
s(1564) =< aux(285)
s(1565) =< aux(283)
s(1566) =< aux(285)
s(1567) =< aux(285)-1
s(1568) =< s(1463)*s(1509)
s(1569) =< s(1463)*aux(285)
s(1570) =< s(1463)*s(1566)
s(1571) =< s(1463)*s(1567)
s(1572) =< s(1571)+s(1569)+aux(283)
s(1573) =< s(1571)+s(1569)+aux(283)
s(1574) =< s(1568)+s(1568)+aux(285)
s(1573) =< s(1568)+s(1568)+aux(285)
s(1565) =< s(1571)+s(1569)+aux(283)
s(1572) =< s(1565)*s(1566)
s(1574) =< s(1565)*s(1566)
s(1575) =< s(1565)*s(1477)
s(1576) =< s(1570)
s(1577) =< s(1573)
s(1578) =< s(1574)
s(1579) =< s(1572)
s(1580) =< s(1569)
s(1581) =< aux(283)
s(1582) =< aux(278)
s(1583) =< aux(278)-1
s(1584) =< s(1463)*s(1503)
s(1585) =< s(1463)*aux(278)
s(1586) =< s(1463)*s(1582)
s(1587) =< s(1463)*s(1583)
s(1588) =< s(1587)+s(1585)
s(1589) =< s(1587)+s(1585)
s(1590) =< s(1584)+s(1584)+aux(278)
s(1589) =< s(1584)+s(1584)+aux(278)
s(1581) =< s(1587)+s(1585)
s(1588) =< s(1581)*s(1582)
s(1590) =< s(1581)*s(1582)
s(1591) =< s(1581)*s(1477)
s(1592) =< s(1586)
s(1593) =< s(1589)
s(1594) =< s(1590)
s(1595) =< s(1588)
s(1596) =< s(1585)
s(1597) =< aux(283)
s(1598) =< s(1521)+s(1517)+aux(283)
s(1599) =< s(1521)+s(1517)+aux(283)
s(1600) =< s(1516)+s(1516)+aux(279)
s(1599) =< s(1516)+s(1516)+aux(279)
s(1597) =< s(1521)+s(1517)+aux(283)
s(1598) =< s(1597)*s(1513)
s(1600) =< s(1597)*s(1513)
s(1601) =< s(1597)*s(1477)
s(1602) =< s(1599)
s(1603) =< s(1600)
s(1604) =< s(1598)
s(1629) =< aux(278)
s(1633) =< s(1497)*aux(282)
s(1634) =< s(1497)*aux(279)
s(1635) =< s(1497)*aux(278)
s(1636) =< s(1497)*s(1513)
s(1637) =< s(1497)*s(1582)
s(1638) =< s(1497)*s(1515)
s(1639) =< s(1638)+s(1634)+aux(278)
s(1640) =< s(1638)+s(1634)+aux(278)
s(1641) =< s(1633)+s(1633)+aux(279)
s(1640) =< s(1633)+s(1633)+aux(279)
s(1629) =< s(1638)+s(1634)+aux(278)
s(1639) =< s(1629)*s(1513)
s(1641) =< s(1629)*s(1513)
s(1642) =< s(1629)*s(1582)
s(1643) =< s(1636)
s(1644) =< s(1640)
s(1645) =< s(1641)
s(1646) =< s(1639)
s(1647) =< s(1634)
s(1650) =< aux(278)
s(1653) =< s(1497)*s(1619)
s(1654) =< s(1497)*aux(281)
s(1655) =< s(1497)*s(1534)
s(1656) =< s(1497)*s(1535)
s(1657) =< s(1656)+s(1654)+aux(278)
s(1658) =< s(1656)+s(1654)+aux(278)
s(1659) =< s(1653)+s(1653)+aux(281)
s(1658) =< s(1653)+s(1653)+aux(281)
s(1650) =< s(1656)+s(1654)+aux(278)
s(1657) =< s(1650)*s(1534)
s(1659) =< s(1650)*s(1534)
s(1660) =< s(1650)*s(1582)
s(1661) =< s(1655)
s(1662) =< s(1658)
s(1663) =< s(1659)
s(1664) =< s(1657)
s(1665) =< s(1654)
s(1666) =< aux(278)
s(1669) =< s(1497)*s(1613)
s(1670) =< s(1497)*aux(283)
s(1671) =< s(1497)*s(1477)
s(1672) =< s(1497)*s(1550)
s(1673) =< s(1672)+s(1670)
s(1674) =< s(1672)+s(1670)
s(1675) =< s(1669)+s(1669)+aux(283)
s(1674) =< s(1669)+s(1669)+aux(283)
s(1666) =< s(1672)+s(1670)
s(1673) =< s(1666)*s(1477)
s(1675) =< s(1666)*s(1477)
s(1676) =< s(1666)*s(1582)
s(1677) =< s(1671)
s(1678) =< s(1674)
s(1679) =< s(1675)
s(1680) =< s(1673)
s(1681) =< s(1670)
s(1683) =< aux(278)
s(1686) =< s(1497)*s(1615)
s(1687) =< s(1497)*aux(285)
s(1688) =< s(1497)*s(1566)
s(1689) =< s(1497)*s(1567)
s(1690) =< s(1689)+s(1687)+aux(283)
s(1691) =< s(1689)+s(1687)+aux(283)
s(1692) =< s(1686)+s(1686)+aux(285)
s(1691) =< s(1686)+s(1686)+aux(285)
s(1683) =< s(1689)+s(1687)+aux(283)
s(1690) =< s(1683)*s(1566)
s(1692) =< s(1683)*s(1566)
s(1693) =< s(1683)*s(1582)
s(1694) =< s(1688)
s(1695) =< s(1691)
s(1696) =< s(1692)
s(1697) =< s(1690)
s(1698) =< s(1687)
s(1699) =< aux(279)
s(1700) =< s(1499)*s(1624)
s(1701) =< s(1499)*aux(279)
s(1702) =< s(1499)*aux(279)
s(1703) =< s(1499)*s(1513)
s(1704) =< s(1499)*s(1513)
s(1705) =< s(1499)*s(1515)
s(1706) =< s(1705)+s(1701)+aux(278)
s(1707) =< s(1705)+s(1701)+aux(278)
s(1708) =< s(1700)+s(1700)+aux(279)
s(1707) =< s(1700)+s(1700)+aux(279)
s(1699) =< s(1705)+s(1701)+aux(278)
s(1706) =< s(1699)*s(1513)
s(1708) =< s(1699)*s(1513)
s(1709) =< s(1699)*s(1513)
s(1710) =< s(1703)
s(1711) =< s(1707)
s(1712) =< s(1708)
s(1713) =< s(1706)
s(1714) =< s(1701)
s(1715) =< aux(279)
s(1716) =< s(1499)*s(1620)
s(1717) =< s(1499)*aux(281)
s(1718) =< s(1499)*s(1534)
s(1719) =< s(1499)*s(1535)
s(1720) =< s(1719)+s(1717)+aux(278)
s(1721) =< s(1719)+s(1717)+aux(278)
s(1722) =< s(1716)+s(1716)+aux(281)
s(1721) =< s(1716)+s(1716)+aux(281)
s(1715) =< s(1719)+s(1717)+aux(278)
s(1720) =< s(1715)*s(1534)
s(1722) =< s(1715)*s(1534)
s(1723) =< s(1715)*s(1513)
s(1724) =< s(1718)
s(1725) =< s(1721)
s(1726) =< s(1722)
s(1727) =< s(1720)
s(1728) =< s(1717)
s(1729) =< aux(279)
s(1730) =< s(1499)*s(1614)
s(1731) =< s(1499)*aux(283)
s(1732) =< s(1499)*s(1477)
s(1733) =< s(1499)*s(1550)
s(1734) =< s(1733)+s(1731)
s(1735) =< s(1733)+s(1731)
s(1736) =< s(1730)+s(1730)+aux(283)
s(1735) =< s(1730)+s(1730)+aux(283)
s(1729) =< s(1733)+s(1731)
s(1734) =< s(1729)*s(1477)
s(1736) =< s(1729)*s(1477)
s(1737) =< s(1729)*s(1513)
s(1738) =< s(1732)
s(1739) =< s(1735)
s(1740) =< s(1736)
s(1741) =< s(1734)
s(1742) =< s(1731)
s(1743) =< aux(279)
s(1744) =< s(1499)*s(1616)
s(1745) =< s(1499)*aux(285)
s(1746) =< s(1499)*s(1566)
s(1747) =< s(1499)*s(1567)
s(1748) =< s(1747)+s(1745)+aux(283)
s(1749) =< s(1747)+s(1745)+aux(283)
s(1750) =< s(1744)+s(1744)+aux(285)
s(1749) =< s(1744)+s(1744)+aux(285)
s(1743) =< s(1747)+s(1745)+aux(283)
s(1748) =< s(1743)*s(1566)
s(1750) =< s(1743)*s(1566)
s(1751) =< s(1743)*s(1513)
s(1752) =< s(1746)
s(1753) =< s(1749)
s(1754) =< s(1750)
s(1755) =< s(1748)
s(1756) =< s(1745)
s(1757) =< aux(279)
s(1759) =< s(1499)*s(1617)
s(1760) =< s(1499)*aux(278)
s(1761) =< s(1499)*s(1582)
s(1762) =< s(1499)*s(1583)
s(1763) =< s(1762)+s(1760)
s(1764) =< s(1762)+s(1760)
s(1765) =< s(1759)+s(1759)+aux(278)
s(1764) =< s(1759)+s(1759)+aux(278)
s(1757) =< s(1762)+s(1760)
s(1763) =< s(1757)*s(1582)
s(1765) =< s(1757)*s(1582)
s(1766) =< s(1757)*s(1513)
s(1767) =< s(1761)
s(1768) =< s(1764)
s(1769) =< s(1765)
s(1770) =< s(1763)
s(1771) =< s(1760)
s(1772) =< aux(279)
s(1773) =< s(1705)+s(1701)+aux(283)
s(1774) =< s(1705)+s(1701)+aux(283)
s(1775) =< s(1700)+s(1700)+aux(279)
s(1774) =< s(1700)+s(1700)+aux(279)
s(1772) =< s(1705)+s(1701)+aux(283)
s(1773) =< s(1772)*s(1513)
s(1775) =< s(1772)*s(1513)
s(1776) =< s(1772)*s(1513)
s(1777) =< s(1774)
s(1778) =< s(1775)
s(1779) =< s(1773)
s(1786) =< aux(278)
s(1789) =< s(1497)*s(1781)
s(1790) =< s(1497)*aux(278)
s(1792) =< s(1497)*s(1582)
s(1794) =< s(1497)*s(1583)
s(1795) =< s(1794)+s(1790)
s(1796) =< s(1794)+s(1790)
s(1797) =< s(1789)+s(1789)+aux(278)
s(1796) =< s(1789)+s(1789)+aux(278)
s(1786) =< s(1794)+s(1790)
s(1795) =< s(1786)*s(1582)
s(1797) =< s(1786)*s(1582)
s(1798) =< s(1786)*s(1582)
s(1799) =< s(1792)
s(1800) =< s(1796)
s(1801) =< s(1797)
s(1802) =< s(1795)
s(1803) =< s(1790)
s(1806) =< aux(278)
s(1813) =< s(1638)+s(1634)+aux(283)
s(1814) =< s(1638)+s(1634)+aux(283)
s(1815) =< s(1633)+s(1633)+aux(279)
s(1814) =< s(1633)+s(1633)+aux(279)
s(1806) =< s(1638)+s(1634)+aux(283)
s(1813) =< s(1806)*s(1513)
s(1815) =< s(1806)*s(1513)
s(1816) =< s(1806)*s(1582)
s(1818) =< s(1814)
s(1819) =< s(1815)
s(1820) =< s(1813)
s(1462) =< s(1458)
s(1865) =< aux(283)
s(1869) =< s(1463)*aux(284)
s(1870) =< s(1463)*aux(287)
s(1872) =< s(1463)*s(1476)
s(1874) =< s(1463)*s(1478)
s(1875) =< s(1874)+s(1870)+aux(286)
s(1876) =< s(1874)+s(1870)+aux(286)
s(1877) =< s(1869)+s(1869)+aux(287)
s(1876) =< s(1869)+s(1869)+aux(287)
s(1865) =< s(1874)+s(1870)+aux(286)
s(1875) =< s(1865)*s(1476)
s(1877) =< s(1865)*s(1476)
s(1878) =< s(1865)*s(1477)
s(1879) =< s(1872)
s(1880) =< s(1876)
s(1881) =< s(1877)
s(1882) =< s(1875)
s(1883) =< s(1870)
s(1886) =< s(1858)
s(1887) =< aux(283)
s(1888) =< s(1858)
s(1889) =< s(1858)-1
s(1890) =< s(1463)*s(1854)
s(1891) =< s(1463)*s(1858)
s(1892) =< s(1463)*s(1888)
s(1893) =< s(1463)*s(1889)
s(1894) =< s(1893)+s(1891)+aux(286)
s(1895) =< s(1893)+s(1891)+aux(286)
s(1896) =< s(1890)+s(1890)+s(1858)
s(1895) =< s(1890)+s(1890)+s(1858)
s(1887) =< s(1893)+s(1891)+aux(286)
s(1894) =< s(1887)*s(1888)
s(1896) =< s(1887)*s(1888)
s(1897) =< s(1887)*s(1477)
s(1898) =< s(1892)
s(1899) =< s(1895)
s(1900) =< s(1896)
s(1901) =< s(1894)
s(1902) =< s(1891)
s(1903) =< aux(283)
s(1904) =< aux(288)
s(1905) =< aux(288)-1
s(1906) =< s(1463)*s(1855)
s(1907) =< s(1463)*aux(288)
s(1908) =< s(1463)*s(1904)
s(1909) =< s(1463)*s(1905)
s(1910) =< s(1909)+s(1907)
s(1911) =< s(1909)+s(1907)
s(1912) =< s(1906)+s(1906)+aux(288)
s(1911) =< s(1906)+s(1906)+aux(288)
s(1903) =< s(1909)+s(1907)
s(1910) =< s(1903)*s(1904)
s(1912) =< s(1903)*s(1904)
s(1913) =< s(1903)*s(1477)
s(1914) =< s(1908)
s(1915) =< s(1911)
s(1916) =< s(1912)
s(1917) =< s(1910)
s(1918) =< s(1907)
s(1919) =< s(1859)
s(1920) =< aux(283)
s(1921) =< s(1859)
s(1922) =< s(1859)-1
s(1923) =< s(1463)*s(1856)
s(1924) =< s(1463)*s(1859)
s(1925) =< s(1463)*s(1921)
s(1926) =< s(1463)*s(1922)
s(1927) =< s(1926)+s(1924)+aux(288)
s(1928) =< s(1926)+s(1924)+aux(288)
s(1929) =< s(1923)+s(1923)+s(1859)
s(1928) =< s(1923)+s(1923)+s(1859)
s(1920) =< s(1926)+s(1924)+aux(288)
s(1927) =< s(1920)*s(1921)
s(1929) =< s(1920)*s(1921)
s(1930) =< s(1920)*s(1477)
s(1931) =< s(1925)
s(1932) =< s(1928)
s(1933) =< s(1929)
s(1934) =< s(1927)
s(1935) =< s(1924)
s(1944) =< aux(283)
s(1945) =< aux(286)
s(1947) =< aux(286)-1
s(1948) =< s(1463)*s(1936)
s(1949) =< s(1463)*aux(286)
s(1951) =< s(1463)*s(1945)
s(1953) =< s(1463)*s(1947)
s(1954) =< s(1953)+s(1949)
s(1955) =< s(1953)+s(1949)
s(1956) =< s(1948)+s(1948)+aux(286)
s(1955) =< s(1948)+s(1948)+aux(286)
s(1944) =< s(1953)+s(1949)
s(1954) =< s(1944)*s(1945)
s(1956) =< s(1944)*s(1945)
s(1957) =< s(1944)*s(1477)
s(1958) =< s(1951)
s(1959) =< s(1955)
s(1960) =< s(1956)
s(1961) =< s(1954)
s(1962) =< s(1949)
s(1965) =< aux(283)
s(1972) =< s(1874)+s(1870)+aux(288)
s(1973) =< s(1874)+s(1870)+aux(288)
s(1974) =< s(1869)+s(1869)+aux(287)
s(1973) =< s(1869)+s(1869)+aux(287)
s(1965) =< s(1874)+s(1870)+aux(288)
s(1972) =< s(1965)*s(1476)
s(1974) =< s(1965)*s(1476)
s(1975) =< s(1965)*s(1477)
s(1977) =< s(1973)
s(1978) =< s(1974)
s(1979) =< s(1972)
with precondition: [V>=0]
* Chain [60]: 986*s(2044)+1058*s(2045)+60*s(2054)+96*s(2055)+414*s(2074)+13*s(2075)+6*s(2081)+24*s(2083)+1*s(2088)+31*s(2089)+11*s(2090)+6*s(2091)+12*s(2092)+8*s(2093)+264*s(2123)+13*s(2125)+1*s(2138)+31*s(2139)+11*s(2140)+6*s(2141)+12*s(2142)+8*s(2143)+528*s(2175)+13*s(2177)+1*s(2190)+62*s(2191)+11*s(2192)+6*s(2193)+12*s(2194)+16*s(2195)+13*s(2227)+1*s(2240)+31*s(2241)+11*s(2242)+6*s(2243)+12*s(2244)+8*s(2245)+13*s(2275)+1*s(2288)+11*s(2290)+6*s(2291)+12*s(2292)+264*s(2323)+13*s(2325)+1*s(2338)+31*s(2339)+11*s(2340)+6*s(2341)+12*s(2342)+8*s(2343)+25
Such that:s(2066) =< V1+V10
s(2116) =< V1+2*V10
s(2218) =< V1+V19
s(2316) =< V1+2*V19
s(2067) =< V9+2*V10
s(2117) =< V9+4*V10
s(2219) =< V9+2*V19
s(2317) =< V9+4*V19
s(2120) =< 2*V10
s(2320) =< 2*V19
aux(331) =< -V1+V9
aux(332) =< V1+1
aux(333) =< V1+V10+V19
aux(334) =< V9
aux(335) =< V9+2*V10+2*V19
aux(336) =< V10
aux(337) =< V10+V19
aux(338) =< V19
s(2055) =< aux(334)
s(2044) =< aux(336)
s(2074) =< aux(331)
s(2075) =< aux(331)
s(2076) =< aux(336)
s(2077) =< aux(334)
s(2078) =< aux(336)-1
s(2079) =< s(2074)*s(2067)
s(2080) =< s(2074)*aux(336)
s(2081) =< s(2074)*aux(334)
s(2082) =< s(2074)*s(2076)
s(2083) =< s(2074)*s(2077)
s(2084) =< s(2074)*s(2078)
s(2085) =< s(2084)+s(2080)
s(2086) =< s(2084)+s(2080)
s(2087) =< s(2079)+s(2079)+s(2066)
s(2086) =< s(2079)+s(2079)+s(2066)
s(2075) =< s(2084)+s(2080)
s(2085) =< s(2075)*s(2076)
s(2087) =< s(2075)*s(2076)
s(2088) =< s(2075)*s(2077)
s(2089) =< s(2082)
s(2090) =< s(2086)
s(2091) =< s(2087)
s(2092) =< s(2085)
s(2093) =< s(2080)
s(2045) =< aux(338)
s(2123) =< s(2120)
s(2125) =< aux(331)
s(2126) =< s(2120)
s(2128) =< s(2120)-1
s(2129) =< s(2074)*s(2117)
s(2130) =< s(2074)*s(2120)
s(2132) =< s(2074)*s(2126)
s(2134) =< s(2074)*s(2128)
s(2135) =< s(2134)+s(2130)+aux(336)
s(2136) =< s(2134)+s(2130)+aux(336)
s(2137) =< s(2129)+s(2129)+s(2116)
s(2136) =< s(2129)+s(2129)+s(2116)
s(2125) =< s(2134)+s(2130)+aux(336)
s(2135) =< s(2125)*s(2126)
s(2137) =< s(2125)*s(2126)
s(2138) =< s(2125)*s(2077)
s(2139) =< s(2132)
s(2140) =< s(2136)
s(2141) =< s(2137)
s(2142) =< s(2135)
s(2143) =< s(2130)
s(2175) =< aux(337)
s(2177) =< aux(331)
s(2178) =< aux(337)
s(2180) =< aux(337)-1
s(2181) =< s(2074)*aux(335)
s(2182) =< s(2074)*aux(337)
s(2184) =< s(2074)*s(2178)
s(2186) =< s(2074)*s(2180)
s(2187) =< s(2186)+s(2182)+aux(338)
s(2188) =< s(2186)+s(2182)+aux(338)
s(2189) =< s(2181)+s(2181)+aux(333)
s(2188) =< s(2181)+s(2181)+aux(333)
s(2177) =< s(2186)+s(2182)+aux(338)
s(2187) =< s(2177)*s(2178)
s(2189) =< s(2177)*s(2178)
s(2190) =< s(2177)*s(2077)
s(2191) =< s(2184)
s(2192) =< s(2188)
s(2193) =< s(2189)
s(2194) =< s(2187)
s(2195) =< s(2182)
s(2227) =< aux(331)
s(2228) =< aux(338)
s(2230) =< aux(338)-1
s(2231) =< s(2074)*s(2219)
s(2232) =< s(2074)*aux(338)
s(2234) =< s(2074)*s(2228)
s(2236) =< s(2074)*s(2230)
s(2237) =< s(2236)+s(2232)
s(2238) =< s(2236)+s(2232)
s(2239) =< s(2231)+s(2231)+s(2218)
s(2238) =< s(2231)+s(2231)+s(2218)
s(2227) =< s(2236)+s(2232)
s(2237) =< s(2227)*s(2228)
s(2239) =< s(2227)*s(2228)
s(2240) =< s(2227)*s(2077)
s(2241) =< s(2234)
s(2242) =< s(2238)
s(2243) =< s(2239)
s(2244) =< s(2237)
s(2245) =< s(2232)
s(2275) =< aux(331)
s(2285) =< s(2186)+s(2182)+aux(336)
s(2286) =< s(2186)+s(2182)+aux(336)
s(2287) =< s(2181)+s(2181)+aux(333)
s(2286) =< s(2181)+s(2181)+aux(333)
s(2275) =< s(2186)+s(2182)+aux(336)
s(2285) =< s(2275)*s(2178)
s(2287) =< s(2275)*s(2178)
s(2288) =< s(2275)*s(2077)
s(2290) =< s(2286)
s(2291) =< s(2287)
s(2292) =< s(2285)
s(2323) =< s(2320)
s(2325) =< aux(331)
s(2326) =< s(2320)
s(2328) =< s(2320)-1
s(2329) =< s(2074)*s(2317)
s(2330) =< s(2074)*s(2320)
s(2332) =< s(2074)*s(2326)
s(2334) =< s(2074)*s(2328)
s(2335) =< s(2334)+s(2330)+aux(338)
s(2336) =< s(2334)+s(2330)+aux(338)
s(2337) =< s(2329)+s(2329)+s(2316)
s(2336) =< s(2329)+s(2329)+s(2316)
s(2325) =< s(2334)+s(2330)+aux(338)
s(2335) =< s(2325)*s(2326)
s(2337) =< s(2325)*s(2326)
s(2338) =< s(2325)*s(2077)
s(2339) =< s(2332)
s(2340) =< s(2336)
s(2341) =< s(2337)
s(2342) =< s(2335)
s(2343) =< s(2330)
s(2054) =< aux(332)
with precondition: [V=1,V1>=0,V9>=0]
* Chain [59]: 1
with precondition: [V=2,V1>=0,V9>=0]
* Chain [58]: 1
with precondition: [V1=0,V>=0]
Closed-form bounds of start(V,V1,V9,V10,V19):
-------------------------------------
* Chain [61] with precondition: [V>=0]
- Upper bound: 6546*V+391+98*V*V+186*V*nat(V1)+62*V*nat(V+V1)+nat(V1)*9277+nat(V1)*62*V+nat(V1)*330*nat(V1)+nat(V1)*62*nat(V+V1)+nat(V1)*12*nat(-V+V1)+nat(V9)*1182+nat(V9)*62*nat(V1)+nat(V10)*1408+nat(V10)*62*nat(V1)+nat(V-1)*23*V+nat(V-1)*69*nat(V1)+nat(V-1)*23*nat(V+V1)+nat(nat(V1)+ -1)*23*V+nat(nat(V1)+ -1)*69*nat(V1)+nat(nat(V1)+ -1)*23*nat(V+V1)+nat(nat(V9)+ -1)*23*nat(V1)+nat(nat(V10)+ -1)*23*nat(V1)+nat(2*V-1)*23*V+nat(2*V-1)*69*nat(V1)+nat(2*V-1)*23*nat(V+V1)+nat(nat(2*V1)+ -1)*23*V+nat(nat(2*V1)+ -1)*69*nat(V1)+nat(nat(2*V1)+ -1)*23*nat(V+V1)+nat(nat(2*V9)+ -1)*23*nat(V1)+nat(nat(2*V10)+ -1)*23*nat(V1)+nat(nat(V+V1)+ -1)*46*V+nat(nat(V+V1)+ -1)*138*nat(V1)+nat(nat(V+V1)+ -1)*46*nat(V+V1)+nat(nat(V9+V10)+ -1)*46*nat(V1)+nat(nat(V9+V10)+ -1)*46*nat(-V+V1)+2700*V+124*V*V+372*V*nat(V1)+124*V*nat(V+V1)+nat(2*V1)*1350+nat(2*V1)*62*V+nat(2*V1)*186*nat(V1)+nat(2*V1)*62*nat(V+V1)+nat(2*V9)*270+nat(2*V9)*62*nat(V1)+nat(2*V10)*270+nat(2*V10)*62*nat(V1)+36*V*V+nat(3*V1)*36*nat(V1)+60*V*V+nat(5*V1)*36*nat(V1)+nat(V+V1)*3291+nat(V+V1)*124*V+nat(V+V1)*372*nat(V1)+nat(V+V1)*160*nat(V+V1)+ (10*V+10)+nat(V+2*V1)*12*V+nat(V+3*V1)*12*nat(V+V1)+nat(V+4*V1)*12*V+nat(V+5*V1)*12*nat(V+V1)+nat(V1+2*V9)*12*nat(V1)+nat(V1+2*V10)*12*nat(V1)+nat(V1+4*V9)*12*nat(V1)+nat(V1+4*V10)*12*nat(V1)+nat(V9+V10)*1068+nat(V9+V10)*124*nat(V1)+nat(V9+V10)*124*nat(-V+V1)+nat(-V+V1)*164+nat(2*V+V1)*36*nat(V1)+nat(2*V+3*V1)*72*nat(V1)+nat(3*V+V1)*12*nat(V+V1)+nat(3*V+2*V1)*24*V+nat(3*V+3*V1)*24*nat(V+V1)+nat(4*V+V1)*36*nat(V1)+nat(5*V+V1)*12*nat(V+V1)+nat(V+V9+V10)*12+nat(V1+2*V9+2*V10)*24*nat(V1)+nat(V1+2*V9+2*V10)*24*nat(-V+V1)
- Complexity: n^2
* Chain [60] with precondition: [V=1,V1>=0,V9>=0]
- Upper bound: 96*V9+25+36*V9*nat(-V1+V9)+nat(V10)*1032+nat(V10)*62*nat(-V1+V9)+nat(V19)*1104+nat(V19)*62*nat(-V1+V9)+nat(nat(V10)+ -1)*23*nat(-V1+V9)+nat(nat(V19)+ -1)*23*nat(-V1+V9)+nat(nat(2*V10)+ -1)*23*nat(-V1+V9)+nat(nat(2*V19)+ -1)*23*nat(-V1+V9)+nat(nat(V10+V19)+ -1)*46*nat(-V1+V9)+nat(2*V10)*264+nat(2*V10)*62*nat(-V1+V9)+nat(2*V19)*264+nat(2*V19)*62*nat(-V1+V9)+nat(V1+V10)*6+nat(V1+V19)*6+ (60*V1+60)+nat(V1+2*V10)*6+nat(V1+2*V19)*6+nat(V9+2*V10)*12*nat(-V1+V9)+nat(V9+2*V19)*12*nat(-V1+V9)+nat(V9+4*V10)*12*nat(-V1+V9)+nat(V9+4*V19)*12*nat(-V1+V9)+nat(V10+V19)*528+nat(V10+V19)*124*nat(-V1+V9)+nat(-V1+V9)*492+nat(V1+V10+V19)*12+nat(V9+2*V10+2*V19)*24*nat(-V1+V9)
- Complexity: n^2
* Chain [59] with precondition: [V=2,V1>=0,V9>=0]
- Upper bound: 1
- Complexity: constant
* Chain [58] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant
### Maximum cost of start(V,V1,V9,V10,V19): nat(V9)*96+24+nat(V10)*1032+nat(2*V10)*264+max([nat(V10)*62*nat(-V1+V9)+nat(V9)*36*nat(-V1+V9)+nat(V19)*1104+nat(V19)*62*nat(-V1+V9)+nat(nat(V10)+ -1)*23*nat(-V1+V9)+nat(nat(V19)+ -1)*23*nat(-V1+V9)+nat(nat(2*V10)+ -1)*23*nat(-V1+V9)+nat(nat(2*V19)+ -1)*23*nat(-V1+V9)+nat(nat(V10+V19)+ -1)*46*nat(-V1+V9)+nat(2*V10)*62*nat(-V1+V9)+nat(2*V19)*264+nat(2*V19)*62*nat(-V1+V9)+nat(V1+V10)*6+nat(V1+V19)*6+nat(V1+1)*60+nat(V1+2*V10)*6+nat(V1+2*V19)*6+nat(V9+2*V10)*12*nat(-V1+V9)+nat(V9+2*V19)*12*nat(-V1+V9)+nat(V9+4*V10)*12*nat(-V1+V9)+nat(V9+4*V19)*12*nat(-V1+V9)+nat(V10+V19)*528+nat(V10+V19)*124*nat(-V1+V9)+nat(-V1+V9)*492+nat(V1+V10+V19)*12+nat(V9+2*V10+2*V19)*24*nat(-V1+V9),6546*V+366+98*V*V+186*V*nat(V1)+62*V*nat(V+V1)+nat(V1)*9277+nat(V1)*62*V+nat(V1)*330*nat(V1)+nat(V1)*62*nat(V+V1)+nat(V1)*12*nat(-V+V1)+nat(V9)*1086+nat(V9)*62*nat(V1)+nat(V10)*376+nat(V10)*62*nat(V1)+nat(V-1)*23*V+nat(V-1)*69*nat(V1)+nat(V-1)*23*nat(V+V1)+nat(nat(V1)+ -1)*23*V+nat(nat(V1)+ -1)*69*nat(V1)+nat(nat(V1)+ -1)*23*nat(V+V1)+nat(nat(V9)+ -1)*23*nat(V1)+nat(nat(V10)+ -1)*23*nat(V1)+nat(2*V-1)*23*V+nat(2*V-1)*69*nat(V1)+nat(2*V-1)*23*nat(V+V1)+nat(nat(2*V1)+ -1)*23*V+nat(nat(2*V1)+ -1)*69*nat(V1)+nat(nat(2*V1)+ -1)*23*nat(V+V1)+nat(nat(2*V9)+ -1)*23*nat(V1)+nat(nat(2*V10)+ -1)*23*nat(V1)+nat(nat(V+V1)+ -1)*46*V+nat(nat(V+V1)+ -1)*138*nat(V1)+nat(nat(V+V1)+ -1)*46*nat(V+V1)+nat(nat(V9+V10)+ -1)*46*nat(V1)+nat(nat(V9+V10)+ -1)*46*nat(-V+V1)+2700*V+124*V*V+372*V*nat(V1)+124*V*nat(V+V1)+nat(2*V1)*1350+nat(2*V1)*62*V+nat(2*V1)*186*nat(V1)+nat(2*V1)*62*nat(V+V1)+nat(2*V9)*270+nat(2*V9)*62*nat(V1)+nat(2*V10)*6+nat(2*V10)*62*nat(V1)+36*V*V+nat(3*V1)*36*nat(V1)+60*V*V+nat(5*V1)*36*nat(V1)+nat(V+V1)*3291+nat(V+V1)*124*V+nat(V+V1)*372*nat(V1)+nat(V+V1)*160*nat(V+V1)+ (10*V+10)+nat(V+2*V1)*12*V+nat(V+3*V1)*12*nat(V+V1)+nat(V+4*V1)*12*V+nat(V+5*V1)*12*nat(V+V1)+nat(V1+2*V9)*12*nat(V1)+nat(V1+2*V10)*12*nat(V1)+nat(V1+4*V9)*12*nat(V1)+nat(V1+4*V10)*12*nat(V1)+nat(V9+V10)*1068+nat(V9+V10)*124*nat(V1)+nat(V9+V10)*124*nat(-V+V1)+nat(-V+V1)*164+nat(2*V+V1)*36*nat(V1)+nat(2*V+3*V1)*72*nat(V1)+nat(3*V+V1)*12*nat(V+V1)+nat(3*V+2*V1)*24*V+nat(3*V+3*V1)*24*nat(V+V1)+nat(4*V+V1)*36*nat(V1)+nat(5*V+V1)*12*nat(V+V1)+nat(V+V9+V10)*12+nat(V1+2*V9+2*V10)*24*nat(V1)+nat(V1+2*V9+2*V10)*24*nat(-V+V1)])+1
Asymptotic class: n^2
* Total analysis performed in 7412 ms.